a:Id, T:Type, ds:x:Id fp Type, P:(State(ds)TProp).
T
 AtomFree(Type;T)
 xdom(ds). A=ds(x)   A
 xdom(ds). A=ds(x)   AtomFree(Type;A)
 (s:State(ds). Dec(v:T. P(s,v)))
 Feasible((with ds: ds
 Faction a:T
 Fprecondition a(v) is
 FP s v)) 

latex

Definitions

t  T, True, T, Id, x:A. B(x), locl(a), <a,b>, Knd, s = t, KindDeq, IdDeq, x:AB(x), P  Q, P  Q, x:AB(x), b, P & Q, P  Q, False, left+right, P  Q, false, eqof(d), f(a), A, Top, x:A. B(x), Dec(P), true, b, Prop, p  q, Type, , p  q, Unit, if b t else f fi, f(x), x  dom(f), xdom(f). v=f(x)   P(x;v), AtomFree(T;x), a:A fp B(a), 1of(t), type List, deq-member(eq;x;L), IdLnk, State(ds), 2of(t), (x  l), z != f(x)  P(a;z), M.sframe(k sends <l,tg>), M.frame(k affects x), f(x)?z, Feasible(M), mk-ma, , x : v, (with ds: ds action a:T precondition a(v) is P s v), x. t(x), x.A(x), {x:A| B(x) }, x,y. t(x;y)

Lemmas

decidable wf, fpf-all wf, fpf-dom wf, fpf-trivial-subtype-top, atom-free wf, fpf wf, ma-state wf, IdLnk wf, deq-member wf, eqtt to assert, eqff to assert, bnot thru bor, iff transitivity, assert of band, and functionality wrt iff, assert of bnot, bor wf, false wf, bool wf, band wf, bnot wf, not wf, assert wf, btrue wf, assert of bor, eqof wf, bfalse wf, deq property, id-deq wf, Knd wf, Kind-deq wf, locl wf, squash wf, true wf, Id wf